Definitions | x:A. B(x), P  Q, ma-frame-compat(A;B), M1 M2, P & Q, x dom(f). v=f(x)  P(x;v), 1of(t), 2of(t), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), State(ds), mk-ma, M.state, M.da(a), (s1 s2 mod x), M.dout(l,tg), M.ds(x), t T, Top, Prop,  x. t(x), if b t else f fi, true , false , z != f(x)  P(a;z), MsgA, Valtype(da;k), P Q, A, P  Q, x(s), , Unit, False,  |